Nuprl Lemma : s-insert_wf
11,40
postcript
pdf
T
:Type. subtype_rel(
T
;
)
(
x
:
T
,
L
:(
T
List). s-insert(
x
;
L
)
(
T
List))
latex
Definitions
t
T
,
x
:
A
.
B
(
x
)
,
i
<z
j
,
if
b
then
t
else
f
fi
,
(
i
=
j
)
,
s-insert(
x
;
l
)
,
P
Q
Lemmas
eq
int
wf
,
ifthenelse
wf
,
lt
int
wf
origin
T:Type. subtype_rel(T; 
) 
(x:T, L:(T List). s-insert(x; L) 
(T List)) T:Type. subtype_rel(T; ) (x:T, L:(T List). s-insert(x; L) (T List)) Tx:A. B(x)
j) Q